\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{7}

\chapter{Functors}
\section{Categories}

So far we've only seen only one category---that of types and functions. So let's quickly gather the essential info about a category.

A category is a collection of objects and arrows that go between them. Every pair of composable arrows can be composed. The composition is associative, and there is an identity arrow looping back on every object.

The fact that types and functions form a category can be expressed in Haskell by defining composition as:
\begin{haskell}
(.) :: (b -> c) -> (a -> b) -> (a -> c)
g . f = \x -> g (f x)
\end{haskell}
The composition of two functions \hask{g} after \hask{f} is a new function that first applies \hask{f} to its argument and then applies \hask{g} to the result.

The identity is a polymorphic ``do nothing'' function:
\begin{haskell}
id :: a -> a
id x = x
\end{haskell}
You can easily convince yourself that such composition is associative, and composing with \hask{id} does nothing to a function.

Based on the definition of a category, we can come up with all kinds of weird categories. For instance, there is a category that has no objects and no arrows. It satisfies all the condition of a category vacuously. There's another one that contains a single object and a single arrow (can you guess what arrow it is?). There's one with two unconnected objects, and one where the two objects are connected by a single arrow (plus two identity arrows), and so on. These are example of what I call \index{stick-figure category}stick-figure categories---categories with a small handful of objects and arrows.
\subsection{Category of sets}

We can also strip a category of all arrows (except for the identity arrows). Such a bare-object category is called a \index{discrete category}\emph{discrete} category or a set\footnote{Ignoring ``size'' issues.}. Since we associate arrows with structure, a set is a category with no structure. 

Sets form their own category called \index{Set, category of sets}$\mathbf{Set}$\footnote{Again, ignoring ``size'' issues, in particular the non-existence of the set of all sets.}. The objects in that category are sets, and the arrows are \index{function}functions between sets. Such functions are defined as special kind of relations, which themselves are defined as sets of pairs.

To the lowest approximation, we can model programming in the category of sets. We often think of types as sets of values, and functions as set-theoretical functions. There's nothing wrong with that. In fact all of categorical constructions we've described so far have their set-theoretical roots. The categorical product is a generalization of the cartesian product of sets, the sum is the disjoint union, and so on. 

What category theory offers is more precision: the fine distinction between the structure that is absolutely necessary, and the superfluous details. 

A set-theoretical function, for instance, doesn't fit the definition of a function we work with as programmers. Our functions must have underlying algorithms because they have to be computable by some physical systems, be it computers or a human brains. There are many more set-theoretical functions than there are algorithms. And some algorithms (in Turing-complete languages) may run forever and never produce a result. 

\subsection{Opposite categories}
In programming, the focus is on the category of types and functions, but we can use this category as a starting point to construct other categories. 
 
One such category is called the \emph{opposite} category. This is the category in which all the original arrows are inverted: what is called the source of an arrow in the original category is now called its target, and vice versa. 

The opposite of a category $\mathcal{C}$ is called $\mathcal{C}^{op}$. We've had a glimpse of this category when we discussed duality. The objects of $\mathcal{C}^{op}$ are the same as those of $\mathcal{C}$. 

Whenever there is an arrow $f \colon a \to b$ in $\mathcal{C}$, there is a corresponding arrow $f^{op} \colon b \to a$ in $\mathcal{C}^{op}$. 

The composition $g^{op} \circ f^{op}$ of two such arrows $f^{op} \colon a \to b$ and $g^{op} \colon b \to c$ is given by the arrow $(f \circ g)^{op}$ (notice the reversed order).

The terminal object in  $\mathcal{C}$ is the initial object in $\mathcal{C}^{op}$, the product in  $\mathcal{C}$ is the sum in $\mathcal{C}^{op}$, and so on. 

\subsection{Product categories}

Given two categories $\mathcal{C}$ and $\mathcal{D}$, we can construct a product category $\mathcal{C} \times \mathcal{D}$. The objects in this category are pairs of objects $\langle c, d \rangle $, and the arrows are pairs of arrows. 

If we have an arrow $f \colon c \to c'$ in $\mathcal{C}$ and an arrow $g \colon d \to d'$ in $\mathcal{D}$ then there is a corresponding arrow $\langle f, g \rangle$ in $\mathcal{C} \times \mathcal{D}$.  This arrow goes from $\langle c, d \rangle $ to $\langle c', d' \rangle $, both being objects in $\mathcal{C} \times \mathcal{D}$. Two such arrows can be composed if their components are composable in, respectively, $\mathcal{C}$ and $\mathcal{D}$. An identity arrow is a pair of identity arrows.

The two product categories we're most interested in are $\mathcal{C} \times \mathcal{C}$ and $\mathcal{C}^{op} \times \mathcal{C}$, where $\mathcal{C}$ is our familiar category of types and functions.

In both of these categories, objects are pairs of objects from $\mathcal{C}$. In the first category, $\mathcal{C} \times \mathcal{C}$, a morphism from $\langle a, b \rangle $ to $\langle a', b' \rangle $ is a pair $\langle f \colon a \to a', g \colon b \to b' \rangle $. In the second category, $\mathcal{C}^{op} \times \mathcal{C}$, a morphism is a pair $\langle f \colon a' \to a, g \colon b \to b' \rangle $, in which the first arrow goes in the opposite direction.

\subsection{Slice categories}

In a neatly organized universe, objects are always objects and arrows are always arrows. Except that sometimes sets of arrows can be thought of as objects. But slice categories break this neat separation: they turn individual arrows into objects. 

A slice category $\cat C/c$ describes how a particular object $c$ is seen from the perspective of its category $\cat C$. It's the totality of arrows pointing at $c$. But to specify an arrow we need to specify both of its ends. Since one of these ends is fixed to be $c$, we only have to specify the other.

An object in the  \index{slice category}\emph{slice category} $\mathcal{C}/c$ (also known as an \index{over category}over-category) is a pair $\langle e, p \rangle$, with $p \colon e \to c$.  

An arrow between two objects $\langle e, p \rangle$ and $\langle e', p' \rangle$ is an arrow $f \colon e \to e'$ of $\cat C$, which makes the following triangle commute:

\[
 \begin{tikzcd}
 e
 \arrow[rd, "p"']
 \arrow[rr, "f"]
 && e'
 \arrow[ld, "p'"]
 \\
 &c
  \end{tikzcd}
\]

\subsection{Coslice categories}

There is a dual notion of a \index{coslice category}coslice category $c / \mathcal{C}$, also known as an \index{under-category}under-category. It's a category of arrows emanating from a fixed object $c$. Objects in this category are pairs $\langle a, i \colon c \to a \rangle$. Morphisms in $c / \mathcal{C}$ are arrows that make the relevant  triangles commute.
\[
 \begin{tikzcd}
& c
 \arrow[rd, "j"]
 \arrow[ld, "i"']
 \\
a
\arrow[rr, "f"']
&& b
  \end{tikzcd}
\]

In particular, if the category $\mathcal{C}$ has a terminal object $1$, then the coslice $1 / \mathcal{C}$ has, as objects, global elements of all the objects of $\mathcal{C}$. 


Morphisms of $1/  \mathcal{C}$ that correspond to arrows $f \colon a \to b$ map the set of global elements of $a$ to the set of global elements of $b$.

 \[
 \begin{tikzcd}
& 1
 \arrow[rd, "y"]
 \arrow[ld, "x"']
 \\
a
\arrow[rr, "f"']
&& b
  \end{tikzcd}
\]
In particular, the construction of a coslice category from the category of types and functions justifies our intuition of types as sets of values, with values represented by global elements of types. 

\section{Functors}

We've seen examples of functoriality when discussing algebraic data types. The idea is that such a data type ``remembers'' the way it was created, and we can manipulate this memory by applying an arrow to its ``contents.'' 

In some cases this intuition is very convincing: we think of a product type as a pair that ``contains'' its ingredients. After all, we can retrieve them using projections. 

This is less obvious in the case of function objects. You can visualize a function object as secretly storing all possible results and using the function argument to index into them. A function from \hask{Bool} is obviously equivalent to a pair of values, one for \hask{True} and one for \hask{False}. It's a known programming trick to implement some functions as lookup tables. It's called \emph{memoization}. 

Even though it's not practical to memoize functions that take, say, natural numbers as arguments; we can still conceptualize them as (infinite, or even uncountable) lookup tables.

If you can think of a data type as a container of values, it makes sense to apply a function to transform all these values, and create a transformed container. When this is possible, we say that the data type is \emph{functorial}. 

Again, function types require some more suspension of disbelief. You visualize a function object as a lookup table, keyed by some type. If you want to use another, related type as your key, you need a function that translates the new key to the original key. This is why functoriality of the function object has one of the arrows reversed:
\begin{haskell}
dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b')
dimap f g h = g . h . f
\end{haskell}
You are applying the transformation to a function \hask{h :: a -> b} that has a ``receptor'' that responds to values of type \hask{a}, and you want to use it to process input of type \hask{a'}. This is only possible if you have a converter from \hask{a'} to \hask{a}, namely \hask{f :: a' -> a}.


The idea of a data type ``containing'' values of another type can be also expressed by saying that one data type is paremeterized by another. For instance, the type \hask{List a} is parameterized by the type \hask{a}. 

In other words, \hask{List} maps the type \hask{a} to the type \hask{List a}. \hask{List} by itself, without the argument, is called a \emph{type constructor}. 

\subsection{Functors between categories}
In category theory, a type constructor is modeled as a mapping of objects to objects. It's a function on objects. This is not to be confused with arrows between objects, which are part of the structure of the category. 

In fact, it's easier to imagine a mapping \emph{between} categories. Every object in the source category is mapped to an object in the target category. If $a$ is an object in $\mathcal{C}$, there is a corresponding object $F a$ in $\mathcal{D}$.

A functorial mapping, or a \emph{functor}, not only maps objects but also arrows between them. Every arrow 
\[ f \colon a \to b\]
in the first category has a corresponding arrow in the second category:
\[ F f \colon F a \to F b\]


\[
 \begin{tikzcd}
 a 
 \arrow[d, blue, "f"]
\arrow[rr, dashed]
 && F a
  \arrow[d, red, "F f"]
 \\
 b 
 \arrow[rr, dashed]
&& F b
  \end{tikzcd}
\]
We use the same letter, here $F$, to name both, the mapping of objects and the mapping of arrows. 

If categories distill the essence of \emph{structure}, then functors are mappings that preserve this structure. Objects that are related in the source category are related in the target category. 

The structure of a category is defined by arrows and their composition. Therefore a functor must preserve composition. What is composed in one category:
\[ h = g \circ f \]
should remain composed in the second category:
\[ F h = F (g \circ f) = F g \circ F f \]
We can either compose two arrows in $\mathcal{C}$ and map the composite to $\mathcal{D}$, or we can map individual arrows and then compose them in $\mathcal{D}$. We demand that the result be the same.
\[
 \begin{tikzcd}
 a 
 \arrow[d, "f"]
\arrow[rrr, dashed]
\arrow[dd, bend right = 70, blue, "g \circ f"']
 &&& F a
  \arrow[d, "F f"]
  \arrow[dd, bend left = 70, "F g \circ F f"]
  \arrow[dd, bend right = 70, red, "F (g \circ f)"']
 \\
 b 
 \arrow[d, "g"]
&&& F b
 \arrow[d, "F g"]
 \\
 c
 \arrow[rrr, dashed]
&&& F c
  \end{tikzcd}
\]

Finally, a functor must preserve identity arrows:
\[ F\, id_a = id_{F a} \]

\[
 \begin{tikzcd}
 a 
  \arrow[loop, blue,  "id_a"']
\arrow[rr, dashed]
 && F a
  \arrow[loop, red, "F \, id_{a}"']
  \arrow[loop, controls={+(2.5, 2.6) and +(-2, 2.5)}, "id_{F a}"']
  \end{tikzcd}
\]

These conditions taken together define what it means for a functor to preserve the structure of a category.

It's also important to realize what conditions are \emph{not} part of the definition. For instance, a functor is allowed to map multiple objects into the same object. It can also map multiple arrows into the same arrow, as long as the endpoints match. 

In the extreme, any category can be mapped to a singleton category with one object and one arrow.

Also, not all object or arrows in the target category must be covered by a functor. In the extreme, we can have a functor from the singleton category to any (non-empty) category. Such a functor picks a single object together with its identity arrow.

A \index{constant functor}\emph{constant functor} $\Delta_c$ is an example of a functor that maps all objects from the source category to a single object $c$ in the target category, and all arrows from the source category to a single identity arrow $id_c$.

In category theory, functors are often used to create models of one category inside another. The fact that they can merge multiple objects and arrows into one means that they produce simplified views of the source category. They ``abstract'' some aspects of the source category.

The fact that they may only cover parts of the target category means that the models are embedded in a larger environment.

Functors from some minimalistic, stick-figure, categories can be used to define patterns in larger categories.

\begin{exercise}
Describe a functor whose source is the \index{walking arrow}``walking arrow'' category. It's a stick-figure category with two objects and a single arrow between them (plus the mandatory identity arrows).
\[
 \begin{tikzcd}
 a 
  \arrow[loop,  "id_{a}"']
\arrow[r, "f"]
 & b
  \arrow[loop, "id_{b}"']
  \end{tikzcd}
\]
\end{exercise}
\begin{exercise}
The ``walking iso'' category is just like the ``walking arrow'' category, plus one more arrow going back from $b$ to $a$. Show that a functor from this category always picks an isomorphism in the target category. 
\end{exercise}

\section{Functors in Programming}

Endofunctors are the class of functors that are the easiest to express in a programming language. These are functors that map a category (here, the category of types and functions) to itself. 

\subsection{Endofunctors}
The first part of the endofunctor is the mapping of types to types. This is done using type constructors, which are type-level functions. 

The list type constructor, \hask{List}, maps an arbitrary type \hask{a} to the type \hask{List a}.

The \hask{Maybe} type constructor maps \hask{a} to \hask{Maybe a}.

The second part of an endofunctor is the mapping of arrows. Given a function \hask{a -> b}, we want to be able to define a function \hask{List a -> List b}, or \hask{Maybe a -> Maybe b}. This is the ``functoriality'' property of these data types that we have discussed before. Functoriality lets us \index{lifting}\emph{lift} an arbitrary function to a function between transformed types.

Functoriality can be expressed in Haskell using a \index{\hask{typeclass}}\emph{typeclass}. In this case, the typeclass is parameterized by a type constructor \hask{f} (in Haskell we use lower case names for type-constructor variables). We say that \hask{f} is a \hask{Functor} if there is a corresponding mapping of functions called \hask{fmap}:
\begin{haskell}
class Functor f where
  fmap :: (a -> b) -> (f a -> f b)
\end{haskell}
The compiler knows that \hask{f} is a type constructor because it's applied to types, as in \hask{f a} and \hask{f b}.

To prove to the compiler that a particular type constructor is a \hask{Functor}, we have to provide the implementation of \hask{fmap} for it. This is done by defining an \index{class instance}\index{\hask{instance}}\emph{instance} of the typeclass \hask{Functor}. For example:
\begin{haskell}
instance Functor Maybe where
  fmap g Nothing  = Nothing
  fmap g (Just a) = Just (g a)
\end{haskell}

A functor must also satisfy some laws: it must preserve composition and identity. These laws cannot be expressed in Haskell, but should be checked by the programmer. We have previously seen a definition of \hask{badMap} that didn't satisfy the identity laws, yet it would be accepted by the compiler. It would define an ``unlawful'' instance of \hask{Functor} for the list type constructor \hask{[]}.

\begin{exercise}
Show that \hask{WithInt} is a functor
\begin{haskell}
data WithInt a = WithInt a Int
\end{haskell}
\end{exercise}

There are some elementary functors that might seem trivial, but they serve as building blocks for other functors. 

We have the identity endofunctor that maps all objects to themselves, and all arrows to themselves. 
\begin{haskell}
newtype Identity a = Identity a
\end{haskell}
\begin{exercise}
Show that \hask{Identity} is a \hask{Functor}. Hint: implement the \hask{Functor} instance for it.
\end{exercise}


We also have a constant functor $\Delta_c$ that maps all objects to a single object $c$, and all arrows to the identity arrow on this object. In Haskell, it's a family of functors parameterized by the target object \hask{c}:
\begin{haskell}
data Constant c a = Constant c
\end{haskell}
This type constructor ignores its second argument.


\begin{exercise}
Show that \hask{(Constant c)} is a \hask{Functor}. Hint: The type constructor takes two arguments, but in the \hask{Functor} instance it's partially applied to the first argument. It is functorial in the second argument.
\end{exercise}


\subsection{Bifunctors}

We have also seen data constructors that take two types as arguments: the product and the sum. They were functorial as well, but instead of lifting a single function, they lifted a pair of functions. In category theory, we would define these as functors from the product category $\mathcal{C} \times \mathcal{C}$ to $\mathcal{C}$.

Such functors map a pair of objects to an object, and a pair of arrows to an arrow. 

In Haskell, we treat such functors as members of a separate class called \hask{Bifunctor}.

\begin{haskell}
class Bifunctor f where
  bimap :: (a -> a') -> (b -> b') -> (f a b -> f a' b')
\end{haskell}
Again, the compiler deduces that \hask{f} is a two-argument type constructor because it sees it applied to two types, e.g., \hask{f a b}.

To prove to the compiler that a particular type constructor is a \hask{Bifunctor}, we define an instance. For example, bifunctoriality of a pair can be defined as:
\begin{haskell}
instance Bifunctor (,) where
  bimap g h (a, b) = (g a, h b)
\end{haskell}

\begin{exercise}
Show that \hask{MoreThanA} is a bifunctor.
\begin{haskell}
data MoreThanA a b = More a (Maybe b)
\end{haskell}
\end{exercise}


\subsection{Contravariant functors}

Functors from the opposite category $\mathcal{C}^{op}$ are called \emph{contravariant}. They have the property of lifting arrows that go in the opposite direction. Regular functors are sometimes called \index{covariant functor}\emph{covariant}.

In Haskell, contravariant functors form the typeclass \hask{Contravariant}:
\begin{haskell}
class Contravariant f where
  contramap :: (b -> a) -> (f a -> f b)
\end{haskell}

It's often convenient to think of functors in terms of producers and consumers. In this analogy, a (covariant) functor is a producer. You can turn a producer of \hask{a}'s into a producer of \hask{b}'s by applying (using \hask{fmap}) a function \hask{a->b}. Conversely, to turn a consumer of \hask{a}'s to a consumer of \hask{b}'s you need a function going in the opposite direction, \hask{b->a}. 

Example: A predicate is a function returning \hask{True} or \hask{False}:
\begin{haskell}
newtype Predicate a = Predicate (a -> Bool)
\end{haskell}
It's easy to see that it's a contravariant functor:
\begin{haskell}
instance Contravariant Predicate where
  contramap f (Predicate h) = Predicate (h . f)
\end{haskell}

In practice, the only non-trivial examples of contravariant functors are variations on the theme of function objects. 

One way to tell if a given function type is covariant or contravariant in one of the type arguments is by assigning polarities to the types used in its definition. We say that the return type of a function is in a \emph{positive} position, so it's covariant; and the argument type is in the \emph{negative} position, so it's contravariant. But if you put the whole function object in the negative position of another function, then its polarities get reversed. 

Consider this data type:
\begin{haskell}
newtype Tester a = Tester ((a -> Bool) -> Bool)
\end{haskell}
It has \hask{a} in a double-negative, therefore a positive position. This is why it's a covariant \hask{Functor}. It acts as a producer of \hask{a}'s:

\begin{haskell}
instance Functor Tester where
  fmap f (Tester g) = Tester g'
    where g' h = g (h . f)
\end{haskell}

Notice that parentheses are important here. A similar function \hask{a -> Bool -> Bool} has \hask{a} in a \emph{negative} position. That's because it's a function of \hask{a} returning a function \hask{(Bool -> Bool)}. Equivalently, you may uncurry it to get a function that takes a pair: \hask{(a, Bool) -> Bool}. Either way, \hask{a} ends up in the negative position.

\subsection{Profunctors}

We've seen before that the function type is functorial. It lifts two functions at a time, just like \hask{Bifunctor}, except that one of the functions goes in the opposite direction. 

In category theory this corresponds to a functor from a product of two categories, one of them being the opposite category: it's a functor from $\mathcal{C}^{op} \times \mathcal{C}$. Functors from $\mathcal{C}^{op} \times \mathcal{C}$ to $\mathbf{Set}$ are called \emph{profunctors}.

In Haskell, profunctors form a typeclass:
\begin{haskell}
class Profunctor f where
  dimap :: (a' -> a) -> (b -> b') -> (f a b -> f a' b')
\end{haskell}

You may think of a profunctor as a type that's simultaneously a producer and a consumer. It consumes one type and produces another.

The function type, which can be written as an infix operator \hask{(->)}, is an instance of \hask{Profunctor}
\begin{haskell}
instance Profunctor (->) where
  dimap f g h = g . h . f
\end{haskell}
This is in accordance with our intuition that a function \hask{a->b} consumes arguments of the type \hask{a} and produces results of the type \hask{b}.

In programming, all non-trivial profunctors are variations on the function type. 

\section{The Hom-Functor}

Arrows between any two objects form a set. This set is called a hom-set and is usually written using the name of the category followed by the names of the objects:
\[ \mathcal{C}(a, b) \]

We can interpret the hom-set $\mathcal{C}(a, b)$ as all the ways $b$ can be observed from $a$. 

Another way of looking at hom-sets is to say that they define a mapping that assigns a set $\mathcal{C}(a, b)$ to every pair of objects. Sets themselves are objects in the category $\mathbf{Set}$. So we have a mapping between categories.

This mapping is functorial. To see that, let's consider what happens when we transform the two objects $a$ and $b$. We are interested in a transformation that would map the set $\mathcal{C}(a, b)$ to the set $\mathcal{C}(a', b')$. Arrows in $\mathbf{Set}$ are regular functions, so it's enough to define their action on individual elements of a set. 

An element of $\mathcal{C}(a, b)$ is an arrow $h \colon a \to b$ and an element of $\mathcal{C}(a', b')$ is an arrow $h' \colon a' \to b'$. We know how to transform one into another: we need to pre-compose $h$ with an arrow $g' \colon a' \to a$ and post-compose it with an arrow $g \colon b \to b'$. 

In other words, the mapping that takes a pair $\langle a, b \rangle$ to the set $\mathcal{C}(a, b)$ is a \emph{profunctor}:
\[ \mathcal{C}^{op} \times \mathcal{C} \to \mathbf{Set} \]

Frequently, we are interested in varying only one of the objects, keeping the other fixed. When we fix the source object and vary the target, the result is a functor  that is written as:
\[ \mathcal{C}(a, -) \colon \mathcal{C} \to \mathbf{Set} \]
The action of this functor on an arrow $g \colon b \to b'$ is written as:
\[ \mathcal{C}(a, g) \colon \mathcal{C}(a, b) \to \mathcal{C}(a, b') \]
and is given by post-composition:
\[\mathcal{C}(a, g) = (g \circ -) \]

Varying $b$ means switching focus from one object to another, so the complete functor $\mathcal{C}(a, -)$ combines all the arrows emanating from $a$ into a coherent view of the category from the perspective of $a$. It is ``the world according to $a$.''

Conversely, when we fix the target and vary the source of the hom-functor, we get a contravariant functor:
\[ \mathcal{C}(-, b) \colon \mathcal{C}^{op} \to \mathbf{Set} \]
whose action on an arrow $g' \colon a' \to a$ is written as:
\[ \mathcal{C}(g', b) \colon \mathcal{C}(a, b) \to \mathcal{C}(a', b) \]
and is given by pre-composition:
\[\mathcal{C}(g', b) = (- \circ g') \]

The functor $\mathcal{C}(-, b)$ organizes all the arrows pointing at $b$ into one coherent view. It is the picture of $b$ ``as it's seen by the world.''

We can now reformulate the results from the chapter on isomorphisms. If two objects $a$ and $b$ are isomorphic, then their hom-sets are also isomorphic. In particular:
\[\mathcal{C}(a, x) \cong \mathcal{C}(b, x)\]
and 
\[\mathcal{C}(x, a) \cong \mathcal{C}(x, b)\]
We'll discuss naturality conditions in the next chapter.

Another way of looking at the hom-functor $\cat C(a, -)$ is as an oracle that  provides answers to the question: ``Is $a$ connected to me?'' If the set $\cat C(a, x)$ is empty, the answer is negative: ``$a$ is not connected to $x$.'' Otherwise, every element of the set $\cat C(a, x)$ is a proof that such connection exists. 

Conversely, the contravariant functor $\cat C (-, a)$ answers the question: ``Am I connected to $a$?''

Taken together, the profunctor $\cat C(x, y)$ establishes a \index{proof-relevant relation}\emph{proof-relevant} relation between objects. Every element of the set $\cat C(x, y)$ is a proof that $x$ is connected to $y$. If the set is empty, the two objects are unrelated. 

\section{Functor Composition}

Just like we can compose functions, we can compose functors. Two functors are composable if the target category of one is the source category of the other.

 On objects, functor composition of $G$ after $F$ first applies $F$ to an object, then applies $G$ to the result; and similarly on arrows.
 
 Obviously, you can only compose composable functors. However all \emph{endofunctors} are composable, since their target category is the same as the source category.
 
 In Haskell, a functor is a parameterized data type, so the composition of two functors is again a parameterized data type. On objects, we define:
 \begin{haskell}
newtype Compose g f a = Compose (g (f a))
\end{haskell}
The compiler figures out that \hask{f} and \hask{g} must be type constructors because they are applied to types: \hask{f} is applied to the type parameter \hask{a}, and \hask{g} is applied to the resulting type.

Alternatively, you can tell the compiler that the first two arguments to \hask{Compose} are type constructors. You do this by providing a \index{kind signatures}\emph{kind signature}. You should also import the \hask{Data.Kind} library that defines \hask{Type}:
\begin{haskell}
import Data.Kind
\end{haskell}

A kind signature is just like a type signature, except that it can be used to describe functions operating on types. 

Regular types have the kind \hask{Type}. Type constructors have the kind \hask{Type -> Type}, since they map types to types. 

\hask{Compose} takes two type constructors and produces a type constructor, so its kind signature is:
\begin{haskell}
(Type -> Type) -> (Type -> Type) -> (Type -> Type) 
\end{haskell}
and the full definition is:
\begin{haskell}
data Compose :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) 
  where
    Compose :: (g (f a)) -> Compose g f a
\end{haskell}

Any two type constructors can be composed this way. There is no requirement, at this point, that they be functors. 

However, if we want to lift a function using the composition of type constructors, \hask{g} after \hask{f}, then they must be functors. This requirement is encoded as a constraint in the instance declaration:
\begin{haskell}
instance (Functor g, Functor f) => Functor (Compose g f) where
  fmap h (Compose gfa) = Compose (fmap (fmap h) gfa)
\end{haskell}
The constraint \hask{(Functor g, Functor f)} expresses the condition that both type constructors be instances of the \hask{Functor} class. The constraints are followed by a double arrow. 

The type constructor whose functoriality we are establishing is \hask{Compose f g}, which is a partial application of \hask{Compose} to two functors. 

In the implementation of \hask{fmap}, we pattern match on the data constructor \hask{Compose}. Its argument \hask{gfa} is of the type \hask{g (f a)}. We use one \hask{fmap} to ``get under'' \hask{g}. Then we use \hask{(fmap h)} to get under \hask{f}. The compiler knows which \hask{fmap} to use by analyzing the types. 

You may visualize a composite functor as a container of containers. For instance, the composition of \hask{[]} with \hask{Maybe} is a list of optional values. 

\begin{exercise}
Define a composition of a \hask{Functor} after \hask{Contravariant}. Hint: You can reuse \hask{Compose}, but you have to provide a different instance declaration.
\end{exercise}


\subsection{Category of categories}

We can view functors as arrows between categories. As we've just seen, functors are composable and it's easy to check that this composition is associative. We also have an identity (endo-) functor for every category. So categories themselves seem to form a category, let's call it $\mathbf{Cat}$. 

And this is where mathematicians start worrying about ``size'' issues. It's a shorthand for saying that there are paradoxes lurking around. So the correct incantation is that $\mathbf{Cat}$ is a category of \emph{small} categories. But as long as we are not engaged in proofs of existence, we can ignore size problems.

\end{document}
